package main;

import java.io.BufferedReader;
import java.io.File;
import java.io.FileReader;

public class Decoder {

	
	public static Solution getSolution(String satFilePath, LiteralAlocatorAndMap map) {
		Solution solution = null;
		int numOfVertices = map.getNumOfVertices();
		try {
			BufferedReader br = new BufferedReader(new FileReader(new File(satFilePath)));
			String lastLine = "";
			String line;
			while ((line = br.readLine()) != null){
				if (line.equalsIgnoreCase("UNSAT")){
					break;
				}else{
					lastLine = line;
				}
			}
			
			String[] tokens = lastLine.split(" ");
			
			// Get edges.
			int[][] edges = new int[numOfVertices][numOfVertices];
			int lastEdgeLiteral = map.getNumOfEdgeLiteral();
			for (int i = 0; i < lastEdgeLiteral; i++) {
				if (!tokens[i].equalsIgnoreCase("")){
				
					Integer lit = Integer.parseInt(tokens[i]);
					Pair<Integer, Integer> pair = map.getLiteralsToEdgesMap().get(Math.abs(lit));
					edges[pair.first-1][pair.second-1] = lit>0?1:0;
				}else {
					System.out.println("ERROR : UNSAT!! ->no satisfying assignment was found");
				}
			}
			
			// Get number of edges.
			int[] sumBitLiterals = map.getSumBits();
			int[] sumBits = new int[sumBitLiterals.length];
			int i = 0;
			for (int sumBitLit: sumBitLiterals) {
				Integer lit = Integer.parseInt(tokens[sumBitLit-1]);
				sumBits[i++] = lit;
			}
			double numOfEdges = (Math.pow(numOfVertices, 2) - numOfVertices)/(double)2 - binaryToDecimal(sumBits);
			
			solution = new Solution(numOfVertices, edges, (int)numOfEdges);

		} catch (Exception e) {
			e.printStackTrace();
		}
		return solution;
	}
	
	public static int binaryToDecimal(int[] sumBits){
		int numOfEdges = 0;
		
		for (int i = 0; i<sumBits.length; i++){
			int bit = -1;
			int lit = sumBits[i];
			if (lit>0)
				bit = 1;
			else
				bit = 0;
			numOfEdges += bit*Math.pow(2, i);
		}
		return numOfEdges;
	}
	
}


